This behavior is intentional. The goal is to detect more type errors arising from a commonly seen pattern like this:

hash = { foo: :bar } #: Hash[Symbol, Symbol]
hash["foo"]          # This is usually a mistake.

I'm open to discuss this issue here to have some conclusion. Do you have any practical examples or real-world scenarios where the proposed one worked better?

(From a type-theoretic perspective, the current implementation (using T) is inconsistent. Having top/untyped is better -- consistent and sound.)

It'd be nice if we could have a signature like:

def []: (K) ->V?
      | (untyped) -> nil

And then that way whenever you use x = hash["foo"] or fail; x + 1 you might get an error because x would be bot

Oh, we do. I opened #1875 a year and a half ago, and that was suggested even before that.

@soutaro any place where you don't control where the argument comes from. I caught this while checking one of the many steep errors i still get on the httpx codename.

Fwiw there are other methods where I'd apply the same reasoning, like Hash#key?, and while I'd expect enforcing typing while make some code a bit more convoluted, I don't see the upside in this case.